Type rule

In type theory, a type rule is a rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well typed and what type expressions have.

Notation

The usual notation have the following general form

\frac{\Gamma_1 \vdash e_1�: \tau_1 \quad \cdots \quad \Gamma_n \vdash e_n�: \tau_n}{\Gamma \vdash e�: \tau}

The first line are the premises that must be fulfilled for the rule to be applied, yielding the second line conclusion. This can be read as, if expression e_i have type \tau_i in environment \Gamma_i (for all i), then an expression e will have a environment \Gamma and type \tau.

For example, a simple language to perform arithmetic calculations on real numbers may have the following rules

\frac{\Gamma \vdash e_1�: real \quad \Gamma \vdash e_2�: real}{\Gamma \vdash e_1%2Be_2�: real} \qquad \frac{\Gamma \vdash e_1�: integer \quad \Gamma \vdash e_2�: integer}{\Gamma \vdash e_1%2Be_2�: integer} \qquad \cdots

A type rule may have no premises, and usually the line is dropped in these cases. A type rule may also specify change a environment by appending the changes to a previous existing environment, for example a declaration may have the following type rule:

\frac{\Gamma \vdash e'�: \tau' \quad \Gamma \vdash e�: \tau}{\Gamma, id�: \tau' \vdash \text{let id = } e' \text{ in } e \text{ end}�: \tau}

This types can be used to derive composed expressions types, much like in natural deduction.

See also

Further reading